// Copyright 2019 - University of Strathclyde, King's College London and Schlumberger Ltd
// This source code is licensed under the BSD license found in the LICENSE file in the root directory of this source tree.

#include "TimSupport.h"
#include "FastEnvironment.h"
#include "Partitions.h"
#include "ptree.h"
#include <numeric>
#include <set>

using std::copy;
using std::greater;
using std::inserter;
using std::max_element;
using std::min_element;
using std::set;

#include <assert.h>

namespace TIM {

  using namespace VAL;

  ostream &operator<<(ostream &o, const Property &p) {
    p.write(o);
    return o;
  };

  int getId(parameter_symbol *s) {
    const IDsymbol< var_symbol > *i =
        dynamic_cast< const IDsymbol< var_symbol > * >(s);
    if (!i) return -1;
    return i->getId();
  };

  template < class T >
  TIMpredSymbol *findPred(T *g);

  template <>
  TIMpredSymbol *findPred(simple_effect *g) {
    return static_cast< TIMpredSymbol * >(
        const_cast< pred_symbol * >(g->prop->head));
  };

  template <>
  TIMpredSymbol *findPred(derivation_rule *g) {
    return static_cast< TIMpredSymbol * >(
        const_cast< pred_symbol * >(g->get_head()->head));
  };

  bool PropertySpace::contains(TIMobjectSymbol *t) const {
    return binary_search(objects.begin(), objects.end(), t);
  };

  struct recordObjectIn {
    PropertySpace *ps;
    bool added;
    recordObjectIn(PropertySpace *p) : ps(p), added(false){};

    void operator()(TIMobjectSymbol *o) {
      if (!ps->contains(o)) {
        o->addIn(ps);
        ps->add(o);
        added = true;
      };
    };

    operator bool() { return added; };
  };

  var_symbol *getAt(var_symbol_list *ps, int v) {
    var_symbol_list::iterator i = ps->begin();
    for (; v > 0; --v, ++i)
      ;
    return *i;
  };

  parameter_symbol *getAt(parameter_symbol_list *ps, int v) {
    parameter_symbol_list::iterator i = ps->begin();
    for (; v > 0; --v, ++i)
      ;
    return *i;
  };

  TransitionRule::TransitionRule(TIMAnalyser *t, operator_ *o, int v,
                                 PropertyState *e, PropertyState *l,
                                 PropertyState *r, opType ty)
      : tan(t),
        op(o),
        drv(0),
        opt(ty),
        var(v),
        enablers(e),
        lhs(l),
        rhs(r),
        objects(var >= 0 ? tan->getTC().range(getAt(op->parameters, var))
                         : vector< const_symbol * >()){};

  TransitionRule::TransitionRule(TIMAnalyser *t, derivation_rule *o, int v,
                                 PropertyState *e, PropertyState *l,
                                 PropertyState *r, opType ty)
      : tan(t),
        op(0),
        drv(o),
        opt(ty),
        var(v),
        enablers(e),
        lhs(l),
        rhs(r),
        objects(var >= 0 ? tan->getTC().range(getAt(drv->get_head()->args, var))
                         : vector< const_symbol * >()){};

  bool TransitionRule::applicableIn(const PropertyState *ps) const {
    return std::includes(ps->begin(), ps->end(), lhs->begin(), lhs->end());
  };

  struct checkNotApplicable {
    TIMobjectSymbol *tos;

    checkNotApplicable(const_symbol *c)
        : tos(static_cast< TIMobjectSymbol * >(c)){};

    bool operator()(Property *p) {
      return find_if(p->begin(), p->end(),
                     not1(bind2nd(mem_fun(&PropertySpace::contains), tos))) !=
             p->end();
    };
  };

  class RuleObjectIterator {
   private:
    TransitionRule *trule;
    vector< const_symbol * >::iterator obit;

    void findValid() {
      while (obit != trule->objects.end()) {
        if (find_if(trule->enablers->begin(), trule->enablers->end(),
                    checkNotApplicable(*obit)) == trule->enablers->end())
          break;
        ++obit;
      };
    };

   public:
    RuleObjectIterator(TransitionRule *tr)
        : trule(tr), obit(trule->objects.begin()) {
      findValid();
    };

    void toEnd() { obit = trule->objects.end(); };

    RuleObjectIterator &operator++() {
      ++obit;
      findValid();
      return *this;
    };

    TIMobjectSymbol *operator*() {
      return static_cast< TIMobjectSymbol * >(*obit);
    };

    bool operator==(const RuleObjectIterator &roi) const {
      return trule == roi.trule && obit == roi.obit;
    };

    bool operator!=(const RuleObjectIterator &roi) const {
      return trule != roi.trule || obit != roi.obit;
    };
  };

  RuleObjectIterator TransitionRule::endEnabledObjects() {
    RuleObjectIterator i(this);
    i.toEnd();
    return i;
  };

  RuleObjectIterator TransitionRule::beginEnabledObjects() {
    return RuleObjectIterator(this);
  };

  struct extendWithIncrRule {
    PropertySpace *ps;
    bool extended;
    extendWithIncrRule(PropertySpace *p) : ps(p), extended(false){};

    void operator()(TransitionRule *tr) {
      if (tr->isIncreasing()) {
        extended = for_each(tr->beginEnabledObjects(), tr->endEnabledObjects(),
                            recordObjectIn(ps));
      };
    };

    operator bool() { return extended; };
  };

  template < class T >
  T isSuper(const PropertyState *p, T b, T e) {
    while (b != e) {
      if (std::includes(p->begin(), p->end(), (*b)->begin(), (*b)->end()))
        return b;
      ++b;
    };
    return b;
  };

  struct extendWithStateRule {
    set< PropertyState * > &got;
    list< PropertyState * > &toExtend;
    PropertyState *prop;

    extendWithStateRule(set< PropertyState * > &s, list< PropertyState * > &l)
        : got(s),
          toExtend(l),
          prop(toExtend.empty() ? 0 : *(toExtend.begin())){};

    void operator()(TransitionRule *tr) {
      if (!prop) return;
      PropertyState *p = tr->tryRule(prop);
      if (p && got.find(p) == got.end()) {
        set< PropertyState * >::const_iterator i =
            isSuper(p, got.begin(), got.end());
        if (i != got.end()) {
          OUTPUT cout << *p
                      << " is a superset of a state we already have: " << **i
                      << "\n";
        } else {
          got.insert(p);
          toExtend.push_back(p);
        };
      };
    };

    void next() {
      toExtend.pop_front();
      prop = toExtend.empty() ? 0 : *(toExtend.begin());
    };

    operator bool() { return !toExtend.empty(); };
  };

  bool PropertySpace::extend() {
    if (!isStateValued) {
      //		cout << "\nExtending attribute space...\n";
      //		write(cout);
      // We add to this space every object that is currently in all of the
      // spaces for enabling properties of any increasing rule in this space.
      bool b = for_each(rules.begin(), rules.end(), extendWithIncrRule(this));
      if (b) sort(objects.begin(), objects.end());
      return b;
    } else {
      //		cout << "\nExtending state space...\n";
      // For each state in the space we need to apply each rule (if it can be
      // applied) and add the corresponding new state to the space. We really
      // should confirm that we only use states for enabled objects, but maybe
      // that's a refinement we can save until later.
      //
      // Basic pattern: for each state and rule pair, if rule applies then
      // produce new state. Key issue: avoid retesting states with rules. One
      // way to do this would be to take each state in turn and extend it with
      // all rules, adding new states to a list as they are generated. As they
      // are added to the list they can also be added to the internal set of
      // states, so that membership can be checked fast.
      list< PropertyState * > toExtend;
      copy(states.begin(), states.end(), inserter(toExtend, toExtend.begin()));
      extendWithStateRule ewsr(this->states, toExtend);
      while (for_each(rules.begin(), rules.end(), ewsr)) ewsr.next();
      //		write(cout);
      return false;
    };
  };

  template <>
  TIMpredSymbol *findPred(simple_goal *g) {
    return static_cast< TIMpredSymbol * >(
        const_cast< pred_symbol * >(g->getProp()->head));
  };

  struct process_argument {
    TIMAnalyser *ta;
    TIMpredSymbol *timps;
    int arg;
    proposition *prp;

    virtual ~process_argument(){};

    template < class T >
    process_argument(TIMAnalyser *t, T *g, proposition *p)
        : ta(t), timps(findPred< T >(g)), arg(0), prp(p){};

    template < class T >
    process_argument(TIMAnalyser *t, T *g)
        : ta(t), timps(findPred< T >(g)), arg(0), prp(0){};

    virtual void operator()(parameter_symbol *p) = 0;
  };

  struct process_argument_in_goal : public process_argument {
    process_argument_in_goal(TIMAnalyser *t, simple_goal *g)
        : process_argument(t, g){};

    virtual ~process_argument_in_goal(){};

    virtual void operator()(parameter_symbol *p) {
      Property *prop = timps->property(arg);
      ++arg;
      ta->insertPre(getId(p), prop);
    };
  };

  struct process_argument_in_effect : public process_argument {
    process_argument_in_effect(TIMAnalyser *t, simple_effect *g)
        : process_argument(t, g){};

    virtual ~process_argument_in_effect(){};

    virtual void operator()(parameter_symbol *p) {
      Property *prop = timps->property(arg);
      ++arg;
      ta->insertEff(getId(p), prop);
    };
  };

  struct process_argument_in_derivation_effect : public process_argument {
    process_argument_in_derivation_effect(TIMAnalyser *t, derivation_rule *g)
        : process_argument(t, g){};

    virtual ~process_argument_in_derivation_effect(){};

    virtual void operator()(parameter_symbol *p) {
      Property *prop = timps->property(arg);
      ++arg;
      ta->insertEff(getId(p), prop);
    };
  };

  struct process_constant_in_goal : public process_argument {
    process_constant_in_goal(TIMAnalyser *t, simple_goal *g)
        : process_argument(t, g){};

    virtual ~process_constant_in_goal(){};

    virtual void operator()(parameter_symbol *p) {
      Property *prop = timps->property(arg);
      ++arg;
      ta->insertGoal(p, prop);
    };
  };

  struct process_constant_in_initial : public process_argument {
    process_constant_in_initial(TIMAnalyser *t, simple_effect *g)
        : process_argument(t, g, g->prop){};

    virtual ~process_constant_in_initial(){};

    virtual void operator()(parameter_symbol *p) {
      Property *prop = timps->property(arg);
      ++arg;
      ta->insertInitial(p, prop, prp);
    };
  };

  void TIMAnalyser::visit_simple_goal(simple_goal *p) {
    if (finally) {
      for_each(p->getProp()->args->begin(), p->getProp()->args->end(),
               process_constant_in_goal(this, p));
    } else {
      for_each(p->getProp()->args->begin(), p->getProp()->args->end(),
               process_argument_in_goal(this, p));
    };
  };

  struct notIn {
    PropertySpace *ps;

    notIn(PropertySpace *p) : ps(p){};

    bool operator()(Property *p) {
      return (p->begin() == p->end()) || *(p->begin()) != ps;
    };
  };

  bool Property::matches(const extended_pred_symbol *eps, pddl_type *pt) {
    if (EPS(predicate)->getParent() != eps->getParent()) return false;
    // cout << "A: " << *pt << "\n";
    // cout << "B: " << *eps << "\n";
    Types::const_iterator tcItr = eps->tcBegin() + posn;
    if (tcItr == eps->tcEnd()) {
      std::cerr
          << "A problem has been encountered with your domain/problem file.\n";
      std::cerr
          << "-------------------------------------------------------------\n";
      std::cerr
          << "Unfortunately, a bug has been encountered in your domain and "
             "problem file,\n";
      std::cerr << "and the planner has to terminate.  The predicate:\n\n";
      std::cerr << "\t" << eps->getName() << "\n\n";
      int realArgs = 0;
      {
        Types::const_iterator tcsItr = eps->tcBegin();
        Types::const_iterator tcsEnd = eps->tcEnd();
        for (; tcsItr != tcsEnd; ++tcsItr) ++realArgs;
      }
      std::cerr << "...takes " << realArgs << " argument";
      if (realArgs != 1) std::cerr << "s";
      std::cerr << ", but has been given at least " << posn + 1 << ".\n";
      exit(0);
    }
    if (*tcItr) {
      //	cout << "C: " << **(eps->tcBegin()+posn) << "\n";
    } else {
      //	cout << "C: ***\n";
      return false;
    };
    return (pt == (*tcItr)->type);
  };

  bool Property::equivalent(const Property *p) const {
    if (this == p) return true;
    if (posn != p->posn ||
        EPS(predicate)->getParent() != EPS(p->predicate)->getParent())
      return false;
    return true;
  };

  struct notMatchFor {
    pddl_type *pt;
    Property *prop;

    notMatchFor(pddl_type *p, Property *pr) : pt(p), prop(pr){};
    bool operator()(extended_pred_symbol *eps) {
      return !(prop->matches(eps, pt));
    };
  };

  struct toProp {
    int arg;

    toProp(int a) : arg(a){};

    Property *operator()(extended_pred_symbol *eps) {
      return static_cast< TIMpredSymbol * >(eps)->property(arg);
    };
  };

  void TIMAnalyser::close(set< Property * > &seed, const pddl_type *pt) {
    bool adding = true;
    while (adding) {
      adding = false;
      PropertyState *ps =
          PropertyState::getPS(this, pt, seed.begin(), seed.end());
      for (TRules::const_iterator r = trules.begin(); r != trules.end(); ++r) {
        if ((*r)->applicableIn(ps)) {
          copy((*r)->getRHS()->begin(), (*r)->getRHS()->end(),
               inserter(seed, seed.begin()));
          adding |= (seed.size() > ps->size());
        };
      };
    };
  };

  vector< Property * > Property::matchers() {
    vector< extended_pred_symbol * > v;
    holding_pred_symbol *h = EPS(predicate)->getParent();

    std::remove_copy_if(
        h->pBegin(), h->pEnd(), inserter(v, v.begin()),
        notMatchFor((*((EPS(predicate)->tBegin()) + posn))->type, this));
    vector< Property * > ps;
    transform(v.begin(), v.end(), inserter(ps, ps.begin()), toProp(posn));
    return ps;
  };

  struct setMatchers {
    vector< Property * > &ps;

    setMatchers(vector< Property * > &p) : ps(p){};

    void operator()(Property *p) {
      vector< Property * > props = p->matchers();
      copy(props.begin(), props.end(), inserter(ps, ps.end()));
    };
  };

  void TIMobjectSymbol::distributeStates(TIMAnalyser *tan) {
    vector< Property * >::iterator s, e, m;
    vector< Property * > matchers;
    for_each(initial.begin(), initial.end(), setMatchers(matchers));
    s = matchers.begin();
    e = matchers.end();

    while (s != e) {
      if ((*s)->begin() == (*s)->end()) {
        // State belonging to no property space.
        // This should not happen...but, see notes.
        ++s;
        continue;
      };
      PropertySpace *p =
          *((*s)->begin());  // Assumes only one space at this stage
      p->add(this);
      m = std::partition(s, e, notIn(p));
      std::sort(m, e);
      PropertyState *ps = PropertyState::getPS(tan, type, m, e);
      p->add(ps);
      e = m;
    };
  };

  Property *Property::getBaseProperty(const pddl_type *pt) const {
    if (!EPS(predicate)->getParent()) return const_cast< Property * >(this);
    TIMpredSymbol *tps =
        static_cast< TIMpredSymbol * >(EPS(predicate)->getParent()->find(
            predicate, makeTT(EPS(predicate)->tBegin(), posn, pt),
            makeTT(EPS(predicate)->tEnd(), 0, 0)));
    return tps->property(posn);
  };

  ostream &operator<<(ostream &o, const TIMobjectSymbol &t) {
    t.write(o);
    return o;
  };

  void TIMAnalyser::visit_simple_effect(simple_effect *p) {
    if (initially) {
      for_each(p->prop->args->begin(), p->prop->args->end(),
               process_constant_in_initial(this, p));
    } else {
      for_each(p->prop->args->begin(), p->prop->args->end(),
               process_argument_in_effect(this, p));
    };
  };

  void TIMAnalyser::visit_simple_derivation_effect(derivation_rule *p) {
    for_each(p->get_head()->args->begin(), p->get_head()->args->end(),
             process_argument_in_derivation_effect(this, p));
  };

  void TIMAnalyser::insertPre(int v, Property *p) {
    if (v < 0) {
      OUTPUT cout << "Property for a constant\n";
      return;
    };
    if (overall) {
      MEX(op)->addInvariant(p, v);
      return;
    } else {
      if (op)
        MEX(op)->addCondition(p, v,
                              isDurative ? (atStart ? START : END) : INSTANT);
    };
    if (!rules[v]) {
      if (op)
        rules[v] = new ProtoRule(
            this, op, v, isDurative ? (atStart ? START : END) : INSTANT);
      if (drv)
        rules[v] = new ProtoRule(
            this, drv, v, isDurative ? (atStart ? START : END) : INSTANT);
    }
    rules[v]->insertPre(p);
  };

  void TIMAnalyser::insertEff(int v, Property *p) {
    if (v < 0) {
      OUTPUT cout << "Property for a constant\n";
      return;
    };
    if (!rules[v]) {
      if (op)
        rules[v] = new ProtoRule(
            this, op, v, isDurative ? (atStart ? START : END) : INSTANT);
      if (drv)
        rules[v] = new ProtoRule(
            this, drv, v, isDurative ? (atStart ? START : END) : INSTANT);
    }
    if (adding) {
      rules[v]->insertAdd(p);
    } else {
      rules[v]->insertDel(p);
    };
  };

  void TIMAnalyser::insertGoal(parameter_symbol *c, Property *p) {
    TIMobjectSymbol *cc = dynamic_cast< TIMobjectSymbol * >(c);

    cc->addFinal(p);
  };

  void TIMAnalyser::insertInitial(parameter_symbol *c, Property *p,
                                  proposition *prp) {
    TIMobjectSymbol *cc = dynamic_cast< TIMobjectSymbol * >(c);

    cc->addInitial(p, prp);
  };

  ostream &operator<<(ostream &o, const PropertyState &p) {
    p.write(o);
    return o;
  };

  ostream &operator<<(ostream &o, const TransitionRule &tr) {
    tr.write(o);
    return o;
  };

  void ProtoRule::addRules(TRules &trules) {
    sort(enablers.begin(), enablers.end());
    sort(adds.begin(), adds.end());
    sort(dels.begin(), dels.end());
    vector< Property * > es;
    set_difference(enablers.begin(), enablers.end(), dels.begin(), dels.end(),
                   inserter(es, es.begin()));
    vector< Property * > is;
    set_intersection(dels.begin(), dels.end(), adds.begin(), adds.end(),
                     inserter(is, is.begin()));
    // Problem here: if we have a constant we still need to know what it is...
    parameter_symbol *v = (var >= 0 ? (op ? getAt(op->parameters, var)
                                          : getAt(drv->get_head()->args, var))
                                    : 0);
    vector< const pddl_type * > types(tan->getTC().leaves(v->type));
    if (types.empty()) types.push_back(v->type);
    if (is.size() > 1 ||
        ((is.size() == 1) && (dels.size() > 1 || adds.size() > 1))) {
      assert(op);
      // don't worry, cannot ever be true for derivation rules: have no delete
      // effects, so is empty, dels empty....
      for (vector< Property * >::iterator i = is.begin(); i != is.end(); ++i) {
        Property *p = *i;
        if (find(enablers.begin(), enablers.end(), p) != enablers.end()) {
          enablers.erase(find(enablers.begin(), enablers.end(), p));
        };
        // Else we are deleting a non-precondition - which could be OK if we
        // are looking at an action end point.
        for (vector< const pddl_type * >::const_iterator pt = types.begin();
             pt != types.end(); ++pt) {
          PropertyState *x = PropertyState::getPS(tan, *pt, i, i + 1);
          PropertyState *en =
              PropertyState::getPS(tan, *pt, enablers.begin(), enablers.end());

          trules.push_back(new TransitionRule(tan, op, var, en, x, x, opt));
        };
        enablers.insert(find_if(enablers.begin(), enablers.end(),
                                bind2nd(greater< Property * >(), p)),
                        p);
      };

      if (adds.size() > is.size() || dels.size() > is.size()) {
        vector< Property * > nadds, ndels;
        set_difference(adds.begin(), adds.end(), is.begin(), is.end(),
                       inserter(nadds, nadds.begin()));
        set_difference(dels.begin(), dels.end(), is.begin(), is.end(),
                       inserter(ndels, ndels.begin()));
        enablers.clear();
        merge(es.begin(), es.end(), is.begin(), is.end(),
              inserter(enablers, enablers.begin()));
        es.swap(enablers);
      } else {
        // No other rule to construct (all in split forms).
        return;
      };
    };
    for (vector< const pddl_type * >::const_iterator pt = types.begin();
         pt != types.end(); ++pt) {
      PropertyState *e = PropertyState::getPS(tan, *pt, es.begin(), es.end());
      PropertyState *l =
          PropertyState::getPS(tan, *pt, dels.begin(), dels.end());
      PropertyState *r =
          PropertyState::getPS(tan, *pt, adds.begin(), adds.end());
      if (op) {
        trules.push_back(new TransitionRule(tan, op, var, e, l, r, opt));
      } else {
        trules.push_back(new TransitionRule(tan, drv, var, e, l, r, opt));
      }
    };
  };

  PropertyState::PMap PropertyState::pmap;

  PropertySpace *PSCombiner(PropertySpace *p1, PropertySpace *p2) {
    p1->merge(p2);
    return p1;
  };

  typedef PropertySpace *(*PSC)(PropertySpace *, PropertySpace *);

  typedef Partitioner< Property *, PropertySpace *, PSC > PM;

  struct unifyWith {
    PM &pm;
    Property *pr;
    TransitionRule *trl;

    unifyWith(PM &p, Property *pp, TransitionRule *tr)
        : pm(p), pr(pp), trl(tr){};

    void operator()(Property *p) {
      if (!pm.contains(p)) {
        pm.add(p, new PropertySpace(p, trl));
      } else {
        // cout << "Adding rule " << *trl << " to " << *(pm.getData(p)) << "\n";
        pm.getData(p)->add(trl);
      };
      pm.connect(pr, p);
    };
  };

  struct makeSpace {
    PM &pm;

    makeSpace(PM &p) : pm(p){};

    void operator()(Property *p) {
      if (!pm.contains(p)) {
        pm.add(p, new PropertySpace(p));
      };
    };
  };

  struct rulePartitioner {
    PM &pm;
    rulePartitioner(PM &p) : pm(p){};

    void operator()(TransitionRule *tr) {
      if (tr->isTrivial()) {
        tr->distributeEnablers();
        return;
      };
      Property *p =
          tr->isIncreasing() ? *(tr->rhs->begin()) : *(tr->lhs->begin());

      for_each(tr->lhs->begin(), tr->lhs->end(), unifyWith(pm, p, tr));
      for_each(tr->rhs->begin(), tr->rhs->end(), unifyWith(pm, p, tr));
      for_each(tr->enablers->begin(), tr->enablers->end(), makeSpace(pm));
    };
  };

  void TransitionRule::distributeEnablers() {
    if (op) {
      MutexStore *m = MEX(op);
      // The enabler mRecs in an op record the enabling property, the variable
      // affected by the rule that is enabled and the part of the operator the
      // rule comes from: START, MIDDLE or END
      m->add(enablers->begin(), enablers->end(), var, opt);
    }
  };

  PropertySpace::PropertySpace(Property *p, TransitionRule *t)
      : properties(1, p), isStateValued(!t->isAttribute()), LSchecked(false) {
    rules.insert(t);
  };

  void PropertySpace::add(TransitionRule *t) {
    rules.insert(t);
    isStateValued &= !t->isAttribute();
  };

  void PropertySpace::write(ostream &o) const {
    o << "\nState space states:\n";
    for_each(states.begin(), states.end(), ptrwriter< PropertyState >(o, "\n"));
    o << "\nSpace properties: ";
    for_each(properties.begin(), properties.end(),
             ptrwriter< Property >(o, " "));
    o << "\nSpace objects: ";
    for_each(objects.begin(), objects.end(), ptrwriter< const_symbol >(o, " "));
    o << "\nSpace rules:\n";
    for_each(rules.begin(), rules.end(), ptrwriter< TransitionRule >(o, "\n"));
    o << "Space is: " << (isStateValued ? "state valued" : "attribute valued");
  };

  ostream &operator<<(ostream &o, const PropertySpace &p) {
    p.write(o);
    return o;
  };

  PropertySpace *spaceSet(PM::DataSource &p) {
    return PM::grabData(p)->finalise();
  };

  bool PropertySpace::isLockingSpace() {
    if (LSchecked) return isLS;
    LSchecked = true;

    cout << "Complete check on locking spaces\n";
    return false;
  };

  void TIMAnalyser::setUpSpaces() {
    PM pts(&PSCombiner);

    for_each(trules.begin(), trules.end(), rulePartitioner(pts));

    transform(pts.begin(), pts.end(), inserter(propspaces, propspaces.begin()),
              spaceSet);
    //	for_each(propspaces.begin(),propspaces.end(),ptrwriter<PropertySpace>(cout,"\n"));
  };

  // Need this because assembleMutexes is not const.
  struct aMxs {
    PropertySpace *p;

    aMxs(PropertySpace *ps) : p(ps){};

    void operator()(TransitionRule *tr) { p->assembleMutexes(tr); };

    void operator()(Property *ps) { p->assembleMutexes(ps); };
  };

  struct aMxs1 {
    TransitionRule *tr;

    aMxs1(TransitionRule *t) : tr(t){};

    void operator()(TransitionRule *t) { t->assembleMutex(tr); };
  };

  struct aMxs2 {
    PropertySpace *ps;
    Property *p;

    aMxs2(PropertySpace *tps, Property *tp) : ps(tps), p(tp){};

    void operator()(Property *tp) {
      if (p <= tp) ps->assembleMutexes(p, tp);
    };
  };

  /*
  struct aMxs3 {
          TransitionRule * tr;

          aMxs3(TransitionRule * t) : tr(t) {};

          void operator()(Property * p)
          {
                  for(Property::SpaceIt i = p->begin();i != p->end();++i)
                  {
                          if((*i)->isState())
                          {
                                  cout << *p << " is candidate enabler for
  action " << tr->byWhat()->name->getName() << "\n";
                                  (*i)->assembleMutexes(tr,p);
                          };
                  };
          };
  };


  // tr is enabled by property p which appears in this PropertySpace
  void PropertySpace::assembleMutexes(TransitionRule * tr,Property * p)
  {
          for_each(rules.begin(),rules.end(),aMxs1(tr));
  };
  */

  // This machinery might need to be reviewed to ensure it handles subtypes
  // properly.
  void PropertySpace::assembleMutexes(Property *p1, Property *p2) {
    if (p1 == p2) {
      if (p1->root()->arity() == 1) return;
      // Same property - special case
      SIterator s = begin();
      for (; s != end(); ++s) {
        if ((*s)->count(p1) > 1) {
          break;
        };
      };
      if (s == end()) {
        // Got one...
        OUTPUT cout << "Mutex between " << *p1 << " and " << *p2 << "\n";
        cTPS(p1->root())->setMutex(p1->aPosn(), cTPS(p2->root()), p2->aPosn());
      };
    } else {
      // Different properties
      // If they only ever appear in different states then they are mutex...
      SIterator s = begin();
      for (; s != end(); ++s) {
        if ((*s)->contains(p1) && (*s)->contains(p2)) {
          break;
        };
      };
      if (s == end()) {
        // Got a mutex...
        OUTPUT cout << "Mutex between " << *p1 << " and " << *p2 << "\n";
        cTPS(p1->root())->setMutex(p1->aPosn(), cTPS(p2->root()), p2->aPosn());
        cTPS(p2->root())->setMutex(p2->aPosn(), cTPS(p1->root()), p1->aPosn());
      };
    };
  };

  // This handles the mutexes that arise because an object cannot simultaneously
  // make two different state transitions.
  void TransitionRule::assembleMutex(TransitionRule *tr) {
    if (op) {
      OUTPUT cout << "Mutex caused by rules: " << *this << " ("
                  << this->byWhat()->name->getName() << ") and " << *tr << " ("
                  << tr->byWhat()->name->getName() << ")\n";

      mutex::constructMutex(op, var, tr->op, tr->var, opt, tr->opt);
      mutex::constructMutex(tr->op, tr->var, op, var, tr->opt, opt);
    }
  };

  ostream &operator<<(ostream &o, opType opt) {
    switch (opt) {
      case INSTANT:
        break;
      case START:
        o << "[start]";
        break;
      case END:
        o << "[end]";
        break;
      case MIDDLE:
        o << "[middle]";
        break;
      default:
        break;
    };
    return o;
  };

  void mutex::write(ostream &o) const {
    for (set< mutRec >::const_iterator i = argPairs.begin();
         i != argPairs.end(); ++i) {
      if (op1 == op2) {
        o << "Cannot perform two concurrent '" << op1->name->getName()
          << "'s for same ";
        if (getAt(op1->parameters, i->first)->type) {
          o << getAt(op1->parameters, i->first)->type->getName();
        } else {
          o << i->first << "th argument";
        };
        o << " " << i->one << "-" << i->other << "\n";
      } else {
        o << "Mutex for '" << op1->name->getName() << "' and '"
          << op2->name->getName() << " args: " << i->first << " " << i->second
          << "\n";
        o << "Mutex for '" << op1->name->getName() << "' and '"
          << op2->name->getName() << "' when using same ";
        if (getAt(op1->parameters, i->first)->type) {
          o << getAt(op1->parameters, i->first)->type->getName();
        } else {
          o << i->first << "th argument";
        };
        o << " " << i->one << "-" << i->other << "\n";
      };
    };
  };

  mutex *MutexStore::getMutex(operator_ *o) {
    MutexRecord::iterator m = mutexes.find(o);
    if (m == mutexes.end()) {
      mutex *mx = new mutex(dynamic_cast< operator_ * >(this), o);
      mutexes[o] = mx;
      MEX(o)->mutexes[dynamic_cast< operator_ * >(this)] = mx;
      return mx;
    } else {
      return m->second;
    };
  };

  void MutexStore::showMutexes() {
    operator_ *o = dynamic_cast< operator_ * >(this);
    for (MutexRecord::iterator i = mutexes.begin(); i != mutexes.end(); ++i) {
      if (i->first >= o) {
        cout << *(i->second);
      };
    };
  };

  void showMutex(operator_ *op) {
    TIM::MutexStore *tm = MEX(op);
    if (tm) {
      tm->showMutexes();
    } else {
      cout << "Not an action\n";
    };
  };

  void completeMutexes(operator_ *op) {
    TIM::MutexStore *tm = MEX(op);
    if (tm) tm->additionalMutexes();
  };

  void PropertySpace::assembleMutexes(Property *p) {
    for_each(properties.begin(), properties.end(), aMxs2(this, p));
  };

  // This is going to consider every rule against every rule in a space.
  void PropertySpace::assembleMutexes(TransitionRule *tr) {
    for_each(rules.begin(), rules.end(), aMxs1(tr));
    // This was introduced as a way to handle the additional mutexes, but it is
    // unnecessary.
    //	for_each(tr->getEnablers()->begin(),tr->getEnablers()->end(),
    //					aMxs3(tr));
  };

  void PropertySpace::assembleMutexes() {
    for_each(rules.begin(), rules.end(), aMxs(this));
    for_each(properties.begin(), properties.end(), aMxs(this));
  };

  void TIMAnalyser::assembleMutexes(PropertySpace *p) { p->assembleMutexes(); };

  void TIMAnalyser::recordRulesInActions(PropertySpace *p) {
    p->recordRulesInActions();
  };

  void TransitionRule::recordInAction(PropertySpace *p) {
    TAS(op->name)->addStateChanger(p, this);
  };

  bool TIMactionSymbol::hasRuleFor(int prm) const {
    for (RCiterator i = begin(); i != end(); ++i) {
      if ((*i)->paramNum() == prm) return true;
    };
    return false;
  };

  struct recRiA {
    PropertySpace *ps;
    recRiA(PropertySpace *p) : ps(p){};
    void operator()(TransitionRule *tr) { tr->recordInAction(ps); };
  };

  void PropertySpace::recordRulesInActions() {
    for_each(rules.begin(), rules.end(), recRiA(this));
  };

  struct addMx1 {
    operator_ *op;
    const mRec &pr;

    addMx1(operator_ *o, const mRec &p) : op(o), pr(p){};

    void operator()(PropertySpace *ps) {
      // cout << "Property space: " << *ps << "\n";
      // if(pr.opt == MIDDLE && !ps->isState()) return;
      if (!ps->isState()) return;

      ps->assembleMutexes(op, pr);
    };

    void operator()(TransitionRule *tr) { tr->assembleMutex(op, pr); };
  };

  struct addMx {
    operator_ *mx;

    addMx(operator_ *m) : mx(m){};

    void operator()(const mRec &p) {
      // cout << "For enabler " << *(p.first) << "\n";
      // Work through all the PropertySpaces that p.first belongs to. Recall
      // p.first is an enabler for the operator mx.
      vector< Property * > ps((p.first)->matchers());
      for (vector< Property * >::iterator i = ps.begin(); i != ps.end(); ++i) {
        for_each((*i)->begin(), (*i)->end(), addMx1(mx, p));
      };
    };
  };

  void TransitionRule::assembleMutex(operator_ *o, const mRec &p) {
    mutex::constructMutex(op, var, o, p.second, opt, p.opt);
    mutex::constructMutex(o, p.second, op, var, p.opt, opt);
  };

  void PropertySpace::assembleMutexes(operator_ *op, const mRec &p) {
    // Work through all the rules in the space
    for_each(rules.begin(), rules.end(), addMx1(op, p));
  };

  void MutexStore::additionalMutexes() {
    // Work through all the enabler mRecs of this action
    // cout << "Considering enablers for action: " <<
    // dynamic_cast<operator_*>(this)->name->getName() << "\n";
    for_each(conditions.begin(), conditions.end(),
             addMx(dynamic_cast< operator_ * >(this)));
    // Work through all the invariant mRecs of this action
    for_each(invariants.begin(), invariants.end(),
             addMx(dynamic_cast< operator_ * >(this)));
  };

  bool checkRule(bool x, TransitionRule *tr) {
    return x && !tr->isIncreasing();
  };

  Property *TransitionRule::candidateSplit() {
    if (isIncreasing()) {
      return *(rhs->begin());
    };
    if (isDecreasing()) {
      return *(lhs->begin());
    };
    return 0;
  };

  void recordSV::operator()(Property *p) {
    vector< int > cnts(ps->countsFor(p));
    int mx = cnts.empty() ? 0 : *max_element(cnts.begin(), cnts.end());
    int mn = cnts.empty() ? 0 : *min_element(cnts.begin(), cnts.end());

    p->setSV(mx == 1, mn > 0);
    if (mx == 1) {
      sv.push_back(p);
#ifdef VERBOSE
      cout << *p << " is single valued ";
      if (mn > 0) cout << "and required";
      cout << "\n";
#endif
    };
  };

  bool PropertySpace::examine(vector< PropertySpace * > &as) {
    // Leave this on to remind us to fix it!
    //#ifdef VERBOSE
    if (std::accumulate(rules.begin(), rules.end(), true, checkRule)) {
      OUTPUT cout << "\nPotential pseudo space...\n"
                  << "This will cause problems in several uses of TIM - tell "
                     "Derek to get on with fixing it!\n"
                  << *this << "\n";
    };
    //#endif

    while (!isStateValued && properties.size() > 1) {
      //		cout << "\nMultiple properties...looking for a
      // splitter...\n"; 		cout << "Space is: " << *this << "\n";
      for (set< TransitionRule * >::iterator i = rules.begin();
           i != rules.end(); ++i) {
        Property *p = (*i)->candidateSplit();
        if (p) {
          //				cout << "Splitter is " << *p << "\n";
          PropertySpace *ps = slice(p);
          //				cout << "Split into: " << *ps << "\nand:
          //"
          //<< *this << "\n";
          while (ps->extend())
            ;
          as.push_back(ps);
          break;
        };
      };
    };
    if (isStateValued) {
      if (!isStatic()) {
        while (extend())
          ;
        assembleMutexes();
      };
      return true;
    };
    return false;
  };

  typedef set< PropertyState * > PStates;

  void doExamine::operator()(PropertySpace *p) {
    if (p->examine(newas)) {
      tan->propspaces.push_back(p);
    } else {
      newas.push_back(p);
    };
  };

  template < class TI >
  struct getConditionally {
    bool cond;
    Property *prop;
    TI pit;
    TI terminus;

    getConditionally(bool c, Property *p, TI pt, TI term)
        : cond(c), prop(p), pit(pt), terminus(term) {
      while (pit != terminus && (c ? (*pit == prop) : (*pit != prop))) ++pit;
    };

    Property *operator*() { return *pit; };

    getConditionally< TI > &operator++() {
      ++pit;
      while (pit != terminus && (cond ? (*pit == prop) : (*pit != prop))) ++pit;
      return *this;
    };

    bool operator==(const getConditionally< TI > &x) const {
      return pit == x.pit;
    };

    bool operator!=(const getConditionally< TI > &x) const {
      return pit != x.pit;
    };
  };

  template < class TI >
  getConditionally< TI > getIt(bool c, Property *p, TI x1, TI x2) {
    return getConditionally< TI >(c, p, x1, x2);
  };

  pair< PropertyState *, PropertyState * > PropertyState::split(Property *p) {
    PropertyState *p1 = retrieve(tan, getIt(false, p, begin(), end()),
                                 getIt(false, p, end(), end()));
    PropertyState *p2 = retrieve(tan, getIt(true, p, begin(), end()),
                                 getIt(true, p, end(), end()));
    return make_pair(p1, p2);
  };

  TransitionRule *TransitionRule::splitRule(Property *p) {
    if (find(lhs->begin(), lhs->end(), p) == lhs->end() &&
        find(rhs->begin(), rhs->end(), p) == rhs->end()) {
      return 0;
    };
    //	cout << "This rule splits: " << *this << "\n";

    pair< PropertyState *, PropertyState * > lhss, rhss;
    PropertyState *ens;

    // Need to remove all instances of p from the lhs/rhs of rule. Note that
    // since we split rules that had a property in both sides the only way p can
    // appear in both lhs and rhs is if one or other side contains nothing
    // except p (possibly several copies).
    lhss = lhs->split(p);
    //	cout << "Left splits to " << *(lhss.first) << " and " << *(lhss.second)
    //<< "\n";
    ens = enablers;
    enablers = enablers->add(lhss.first->begin(), lhss.first->end());
    lhs = lhss.second;
    ens = ens->add(lhss.second->begin(), lhss.second->end());
    rhss = rhs->split(p);
    rhs = rhss.second;
    //	cout << "Right splits to " << *(rhss.first) << " and " << *(rhss.second)
    //<< "\n";

    //	cout << "Enablers are now: " << *ens << " and " << *enablers << "\n";
    TransitionRule *trnew =
        new TransitionRule(tan, op, var, ens, lhss.first, rhss.first, opt);
    //	cout << "Objects are: ";
    //	for_each(objects.begin(),objects.end(),ptrwriter<const_symbol>(cout,"
    //")); 	cout << "\n";
    return trnew;
  };

  TransitionRule::TransitionRule(TransitionRule *tr, PropertyState *e,
                                 PropertyState *l, PropertyState *r)
      : tan(tr->tan),
        op(tr->op),
        opt(tr->opt),
        var(tr->var),
        enablers(e),
        lhs(l),
        rhs(r),
        objects(){};

  struct ruleSplitOn {
    set< TransitionRule * > &xrules;
    set< TransitionRule * > rules;
    Property *prop;

    ruleSplitOn(Property *p, set< TransitionRule * > &rs)
        : xrules(rs), prop(p){};

    void operator()(TransitionRule *tr) {
      TransitionRule *t = tr->splitRule(prop);
      if (t) xrules.insert(t);
      if (!tr->isTrivial()) {
        rules.insert(tr);
      };
    };

    operator set< TransitionRule * >() { return rules; };
  };

  void splitRules(set< TransitionRule * > &rules, Property *p,
                  set< TransitionRule * > &xrules) {
    rules = for_each(rules.begin(), rules.end(), ruleSplitOn(p, xrules));
  };

  void splitObjects(vector< TIMobjectSymbol * > &tobs, Property *p,
                    vector< TIMobjectSymbol * > &xtobs){
      // I think we should be checking whether the objects are really valid for
      // both
      // spaces - in particular if the new space is a state space we should be
      // filtering it.
      //
      //	cout << "SYMBOLS: ";
      //	for_each(tobs.begin(),tobs.end(),ptrwriter<const_symbol>(cout,"
      //"));
      //	cout << "\n";
  };

  void splitStates(PStates &states, Property *p, PStates &xstates) {
    PStates::iterator e = states.end();
    PStates newStates;
    for (PStates::iterator i = states.begin(); i != e; ++i) {
      pair< PropertyState *, PropertyState * > pp = (*i)->split(p);
      if (!pp.first->empty()) xstates.insert(pp.first);
      if (!pp.second->empty()) newStates.insert(pp.second);
    };
    states.swap(newStates);
  };

  bool ruleCheck(bool t, TransitionRule *tr) {
    return t && !tr->isAttribute();
  };

  void PropertySpace::checkStateValued() {
    isStateValued = accumulate(rules.begin(), rules.end(), true, ruleCheck);
  };

  PropertySpace *PropertySpace::slice(Property *p) {
    // Also need to remove split property from this space and correct the
    // relevant references to membership of property spaces.
    PropertySpace *ps = new PropertySpace(p);
    ps->isStateValued = false;
    splitStates(states, p, ps->states);
    // cout << "About to split rules in " << *this << "\n";
    splitRules(rules, p, ps->rules);
    // cout << "OBJECTS: ";
    // for_each(objects.begin(),objects.end(),ptrwriter<const_symbol>(cout,"
    // ")); cout << "\n";
    splitObjects(objects, p, ps->objects);
    properties.erase(remove(properties.begin(), properties.end(), p),
                     properties.end());
    checkStateValued();
    return ps;
  };

  bool Property::applicableTo(TypeChecker &tc, const pddl_type *tp) const {
    // Caution: won't work if predicate has an either type spec.
    pddl_type *x = (*(EPS(predicate)->tcBegin() + posn))->type;
    return tc.subType(tp, x);
  };

  bool PropertySpace::applicableTo(TypeChecker &tc, const pddl_type *tp) const {
    for (vector< Property * >::const_iterator i = properties.begin();
         i != properties.end(); ++i) {
      if (!(*i)->applicableTo(tc, tp)) return false;
    };
    return true;
  };

  set< PropertySpace * > TIMAnalyser::relevant(pddl_type *tp) {
    // Really only want to use this on leaf types. Other types are more of a
    // problem at both this end and the caller's end. This is only a temporary
    // management of the situation.
    if (!tcheck.isLeafType(tp)) {
      return set< PropertySpace * >();
    };
    set< PropertySpace * > st;
    for (vector< PropertySpace * >::iterator i = propspaces.begin();
         i != propspaces.end(); ++i) {
      if ((*i)->applicableTo(tcheck, tp)) {
        st.insert(*i);
      };
    };
    return st;
  };

};  // namespace TIM
